Nuprl Definition : monoid_hom_p 13,42
compound
IsMonHom{M1,M2}(f) == FunThru2op(|M1|;|M2|;*;*;f) & f(e) = e 
latex

clarification:

compound
IsMonHom{M1,M2}(f) == FunThru2op(|M1|;|M2|;*M1;*M2;f) & f(eM1) = (eM2)  |M2| 
latex

Upgroups 1
Wellformedness Lemmasmonoid hom p wf
DefinitionsP & Q, FunThru2op(A;B;opa;opb;f), *, |g|, e

origin